($\lambda$$T$,$L_{1}$,$L_{2}$,$L$,$z$. interleaving($T$;$L_{1}$;$L_{2}$;$L$))
\\[0ex]$\in$ $T$:Type$\rightarrow$($T$ List)$\rightarrow$($T$ List)$\rightarrow$($T$ List)$\rightarrow\downarrow$True$\rightarrow$Prop